the_w:World, l:IdLnk, mss:(Msg List). onlnk(l;mss)  (Msg List) 

latex

Definitions	x:A. B(x), Msg, t  T, onlnk(l;mss), w.M, t.1, t.2, World
Lemmas	filter wf, Msg wf, eq lnk wf, mlnk wf, IdLnk wf, world wf